SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Metalogic</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Metalogic</span></span>

</h1>

</header>

<p><b>Metalogic</b> is the <a href="Metatheory" title="Metatheory">metatheory</a> of <a href="Logic" title="Logic">logic</a>. Whereas <i>logic</i> studies how <a href="Formal_system" title="Formal system">logical systems</a> can be used to construct <a href="Validity_(logic)" title="Validity (logic)">valid</a> and <a href="Soundness" title="Soundness">sound</a> <a href="Argument" title="Argument">arguments</a>, metalogic studies the properties of <a href="Logical_system" class="mw-redirect" title="Logical system">logical systems</a>.<sup id="cite_ref-1" class="reference"><a href="#cite_note-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Logic concerns the truths that may be derived using a logical system; metalogic concerns the truths that may be derived <i>about</i> the <a href="Formal_language" title="Formal language">languages</a> and systems that are used to express truths.<sup id="cite_ref-metalogic_2-0" class="reference"><a href="#cite_note-metalogic-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup>

</p><p>The basic objects of metalogical study are formal languages, formal systems, and their <a href="Interpretation_(logic)" title="Interpretation (logic)">interpretations</a>. The study of interpretation of formal systems is the branch of <a href="Mathematical_logic" title="Mathematical logic">mathematical logic</a> that is known as <a href="Model_theory" title="Model theory">model theory</a>, and the study of <a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive systems</a> is the branch that is known as <a href="Proof_theory" title="Proof theory">proof theory</a>.

</p>

<div class="mw-heading mw-heading2"><h2 id="Overview">Overview</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Formal_language">Formal language</h3></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hatnote{font-style:italic}.mw-parser-output div.hatnote{padding-left:1.6em;margin-bottom:0.5em}.mw-parser-output .hatnote i{font-style:normal}.mw-parser-output .hatnote+link+.hatnote{margin-top:-0.5em}@media print{body.ns-0 .mw-parser-output .hatnote{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_language" title="Formal language">Formal language</a></div>

<p>A <i>formal language</i> is an organized set of <a href="Symbol_(formal)" title="Symbol (formal)">symbols</a>, the symbols of which precisely define it by shape and place. Such a language therefore can be defined without <a href="Reference" title="Reference">reference</a> to the <a href="Meaning_(linguistics)" class="mw-redirect" title="Meaning (linguistics)">meanings</a> of its expressions; it can exist before any <a href="Interpretation_(logic)" title="Interpretation (logic)">interpretation</a> is assigned to it—that is, before it has any meaning. <a href="First-order_logic" title="First-order logic">First-order logic</a> is expressed in some formal language. A <a href="Formal_grammar" title="Formal grammar">formal grammar</a> determines which symbols and sets of symbols are <a href="Well-formed_formula" title="Well-formed formula">formulas</a> in a formal language.

</p><p>A formal language can be formally defined as a set <i>A</i> of strings (finite sequences) on a fixed alphabet α. Some authors, including <a href="Rudolf_Carnap" title="Rudolf Carnap">Rudolf Carnap</a>, define the language as the ordered pair <α, <i>A</i>>.<sup id="cite_ref-itslaia_3-0" class="reference"><a href="#cite_note-itslaia-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> Carnap also requires that each element of α must occur in at least one string in <i>A</i>.

</p>

<div class="mw-heading mw-heading3"><h3 id="Formation_rules">Formation rules</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formation_rule" title="Formation rule">Formation rule</a></div>

<p><i>Formation rules</i> (also called <i>formal grammar</i>) are a precise description of the <a href="Well-formed_formula" title="Well-formed formula">well-formed formulas</a> of a formal language. They are synonymous with the <a href="Set_(mathematics)" title="Set (mathematics)">set</a> of <a href="String_(computer_science)" title="String (computer science)">strings</a> over the <a href="Alphabet" title="Alphabet">alphabet</a> of the formal language that constitute well formed formulas. However, it does not describe their <a href="Semantics" title="Semantics">semantics</a> (i.e. what they mean).

</p>

<div class="mw-heading mw-heading3"><h3 id="Formal_systems">Formal systems</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_system" title="Formal system">Formal system</a></div>

<p>A <i>formal system</i> (also called a <i>logical calculus</i>, or a <i>logical system</i>) consists of a formal language together with a <a href="Deductive_system" class="mw-redirect" title="Deductive system">deductive apparatus</a> (also called a <i>deductive system</i>). The deductive apparatus may consist of a set of <a href="Rule_of_inference" title="Rule of inference">transformation rules</a> (also called <i>inference rules</i>) or a set of <a href="Axiom" title="Axiom">axioms</a>, or have both. A formal system is used to <a href="Proof_theory" title="Proof theory">derive</a> one expression from one or more other expressions.

</p><p>A <i>formal system</i> can be formally defined as an ordered triple <α,<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {I}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {I}}}</annotation>

</semantics>

</math></span><img src="./0e9730a0ada0426927ff64141eb9f505eca132d4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-left: -0.069ex; width:1.561ex; height:2.176ex;" alt="{\displaystyle {\mathcal {I}}}" loading="lazy"></span>,<span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {D}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {D}}}</annotation>

</semantics>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {D}}}</annotation>

</semantics>

</math></span><img src="./3277962e1959c3241fb1b70c7f0ac6dcefebd966.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.792ex; height:2.176ex;" alt="{\displaystyle {\mathcal {D}}}" loading="lazy"></span>d is the relation of direct derivability. This relation is understood in a comprehensive <a href="Sense_and_reference" title="Sense and reference">sense</a> such that the primitive sentences of the formal system are taken as directly <a href="Formal_proof" title="Formal proof">derivable</a> from the <a href="Empty_set" title="Empty set">empty set</a> of sentences. Direct derivability is a relation between a sentence and a finite, possibly empty set of sentences. Axioms are so chosen that every first place member of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {D}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {D}}}</annotation>

</semantics>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {I}}}</annotation>

</semantics>

</math></span><img src="./0e9730a0ada0426927ff64141eb9f505eca132d4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-left: -0.069ex; width:1.561ex; height:2.176ex;" alt="{\displaystyle {\mathcal {I}}}" loading="lazy"></span> and every second place member is a finite subset of <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {I}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {I}}}</annotation>

</semantics>

</p><p>A <i>formal system</i> can also be defined with only the relation <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle {\mathcal {D}}}">

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {D}}}</annotation>

</semantics>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle {\mathcal {I}}}</annotation>

</semantics>

</math></span><img src="./0e9730a0ada0426927ff64141eb9f505eca132d4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; margin-left: -0.069ex; width:1.561ex; height:2.176ex;" alt="{\displaystyle {\mathcal {I}}}" loading="lazy"></span> and α in the definitions of <i>interpreted formal language</i>, and <i>interpreted formal system</i>. However, this method can be more difficult to understand and use.<sup id="cite_ref-itslaia_3-1" class="reference"><a href="#cite_note-itslaia-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup>

</p>

<div class="mw-heading mw-heading3"><h3 id="Formal_proofs">Formal proofs</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Formal_proof" title="Formal proof">Formal proof</a></div>

<p>A <i>formal proof</i> is a sequence of well-formed formulas of a formal language, the last of which is a <a href="Theorem" title="Theorem">theorem</a> of a formal system. The theorem is a <a href="Logical_consequence" title="Logical consequence">syntactic consequence</a> of all the well formed formulae that precede it in the proof system. For a well formed formula to qualify as part of a proof, it must result from applying a rule of the deductive apparatus of some formal system to the previous well formed formulae in the proof sequence.

</p>

<div class="mw-heading mw-heading3"><h3 id="Interpretations">Interpretations</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main articles: <a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation (logic)</a> and <a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics (logic)</a></div>

<p>An <i>interpretation</i> of a formal system is the assignment of meanings to the symbols and <a href="Truth_value" title="Truth value">truth-values</a> to the sentences of the formal system. The study of interpretations is called <a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics</a>. <i>Giving an interpretation</i> is synonymous with <i>constructing a <a href="Structure_(mathematical_logic)" title="Structure (mathematical logic)">model</a></i>.

</p>

<div class="mw-heading mw-heading2"><h2 id="Important_distinctions">Important distinctions</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Metalanguage–object_language">Metalanguage–object language</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Metalanguage" title="Metalanguage">Metalanguage</a></div>

<p>In metalogic, formal languages are sometimes called <i>object languages</i>. The language used to make statements about an object language is called a <i>metalanguage</i>. This distinction is a key difference between logic and metalogic. While logic deals with <i>proofs in a formal system</i>, expressed in some formal language, metalogic deals with <i>proofs about a formal system</i> which are expressed in a metalanguage about some object language.

</p>

<div class="mw-heading mw-heading3"><h3 id="Syntax–semantics">Syntax–semantics</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main articles: <a href="Syntax_(logic)" title="Syntax (logic)">Syntax (logic)</a> and <a href="Formal_semantics_(logic)" class="mw-redirect" title="Formal semantics (logic)">Formal semantics (logic)</a></div>

<p>In metalogic, 'syntax' has to do with formal languages or formal systems without regard to any interpretation of them, whereas, 'semantics' has to do with interpretations of formal languages. The term 'syntactic' has a slightly wider scope than 'proof-theoretic', since it may be applied to properties of formal languages without any deductive systems, as well as to formal systems. 'Semantic' is synonymous with 'model-theoretic'.

</p>

<div class="mw-heading mw-heading3"><h3 id="Use–mention">Use–mention</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Use%E2%80%93mention_distinction" title="Use–mention distinction">Use–mention distinction</a></div>

<p>In metalogic, the words <i>use</i> and <i>mention</i>, in both their noun and verb forms, take on a technical sense in order to identify an important distinction.<sup id="cite_ref-metalogic_2-1" class="reference"><a href="#cite_note-metalogic-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> The <i>use–mention distinction</i> (sometimes referred to as the <i>words-as-words distinction</i>) is the distinction between <i>using</i> a word (or phrase) and <i>mentioning</i> it. Usually it is indicated that an expression is being mentioned rather than used by enclosing it in quotation marks, printing it in italics, or setting the expression by itself on a line. The enclosing in quotes of an expression gives us the <a href="Name" title="Name">name</a> of an expression, for example:

</p>

/* start https://en.wikipedia.org/ */

.mw-parser-output .templatequote{overflow:hidden;margin:1em 0;padding:0 32px}.mw-parser-output .templatequotecite{line-height:1.5em;text-align:left;margin-top:0}@media(min-width:500px){.mw-parser-output .templatequotecite{padding-left:1.6em}}

/* end https://en.wikipedia.org/ */

</style><blockquote class="templatequote"><div class="poem">

<p>"Metalogic" is the name of this article.<br>

This article is about metalogic.

</p>

</div></blockquote>

<div class="mw-heading mw-heading3"><h3 id="Type–token">Type–token</h3></div>

<div role="note" class="hatnote navigation-not-searchable">Main article: <a href="Type%E2%80%93token_distinction" title="Type–token distinction">Type–token distinction</a></div>

<p>The <i>type-token distinction</i> is a distinction in metalogic, that separates an abstract concept from the objects which are particular instances of the concept. For example, the particular bicycle in your garage is a token of the <a href="Type%E2%80%93token_distinction" title="Type–token distinction">type</a> of thing known as "The bicycle." Whereas, the bicycle in your garage is in a particular place at a particular time, that is not true of "the bicycle" as used in the sentence: "<i>The bicycle</i> has become more popular recently." This distinction is used to clarify the meaning of <a href="Symbol_(formal)" title="Symbol (formal)">symbols</a> of <a href="Formal_language" title="Formal language">formal languages</a>.

</p>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<p>Metalogical questions have been asked since the time of <a href="Aristotle" title="Aristotle">Aristotle</a>.<sup id="cite_ref-4" class="reference"><a href="#cite_note-4"><span class="cite-bracket">[</span>4<span class="cite-bracket">]</span></a></sup> However, it was only with the rise of formal languages in the late 19th and early 20th century that investigations into the foundations of logic began to flourish. In 1904, <a href="David_Hilbert" title="David Hilbert">David Hilbert</a> observed that in investigating the <a href="Foundations_of_mathematics" title="Foundations of mathematics">foundations of mathematics</a> that logical notions are presupposed, and therefore a simultaneous account of metalogical and <a href="Metamathematics" title="Metamathematics">metamathematical</a> principles was required. Today, metalogic and metamathematics are largely synonymous with each other, and both have been substantially subsumed by <a href="Mathematical_logic" title="Mathematical logic">mathematical logic</a> in academia. A possible alternate, less mathematical model may be found in the writings of <a href="Charles_Sanders_Peirce" title="Charles Sanders Peirce">Charles Sanders Peirce</a> and other <a href="Semiotics" title="Semiotics">semioticians</a>.

</p>

<div class="mw-heading mw-heading2"><h2 id="Results">Results</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .ambox{border:1px solid #a2a9b1;border-left:10px solid #36c;background-color:#fbfbfb;box-sizing:border-box}.mw-parser-output .ambox+link+.ambox,.mw-parser-output .ambox+link+style+.ambox,.mw-parser-output .ambox+link+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+style+.ambox,.mw-parser-output .ambox+.mw-empty-elt+link+link+.ambox{margin-top:-1px}html body.mediawiki .mw-parser-output .ambox.mbox-small-left{margin:4px 1em 4px 0;overflow:hidden;width:238px;border-collapse:collapse;font-size:88%;line-height:1.25em}.mw-parser-output .ambox-speedy{border-left:10px solid #b32424;background-color:#fee7e6}.mw-parser-output .ambox-delete{border-left:10px solid #b32424}.mw-parser-output .ambox-content{border-left:10px solid #f28500}.mw-parser-output .ambox-style{border-left:10px solid #fc3}.mw-parser-output .ambox-move{border-left:10px solid #9932cc}.mw-parser-output .ambox-protection{border-left:10px solid #a2a9b1}.mw-parser-output .ambox .mbox-text{border:none;padding:0.25em 0.5em;width:100%}.mw-parser-output .ambox .mbox-image{border:none;padding:2px 0 2px 0.5em;text-align:center}.mw-parser-output .ambox .mbox-imageright{border:none;padding:2px 0.5em 2px 0;text-align:center}.mw-parser-output .ambox .mbox-empty-cell{border:none;padding:0;width:1px}.mw-parser-output .ambox .mbox-image-div{width:52px}@media(min-width:720px){.mw-parser-output .ambox{margin:0 10%}}@media print{body.ns-0 .mw-parser-output .ambox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style>

<p>Results in metalogic consist of such things as <a href="Formal_proof" title="Formal proof">formal proofs</a> demonstrating the <a href="Consistency" title="Consistency">consistency</a>, <a href="Completeness_(logic)" title="Completeness (logic)">completeness</a>, and <a href="Decidability_(logic)" title="Decidability (logic)">decidability</a> of particular <a href="Formal_system" title="Formal system">formal systems</a>.

</p><p>Major results in metalogic include:

</p>

<ul><li>Proof of the <a href="Uncountability" class="mw-redirect" title="Uncountability">uncountability</a> of the <a href="Power_set" title="Power set">power set</a> of the <a href="Natural_number" title="Natural number">natural numbers</a> (<a href="Cantor's_theorem" title="Cantor's theorem">Cantor's theorem</a> 1891)</li>

<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem theorem</a> (<a href="Leopold_L%C3%B6wenheim" title="Leopold Löwenheim">Leopold Löwenheim</a> 1915 and <a href="Thoralf_Skolem" title="Thoralf Skolem">Thoralf Skolem</a> 1919)</li>

<li>Proof of the consistency of truth-functional <a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">propositional logic</a> (<a href="Emil_Leon_Post" title="Emil Leon Post">Emil Post</a> 1920)</li>

<li>Proof of the semantic completeness of truth-functional propositional logic (<a href="Paul_Bernays" title="Paul Bernays">Paul Bernays</a> 1918),<sup id="cite_ref-reflections_5-0" class="reference"><a href="#cite_note-reflections-5"><span class="cite-bracket">[</span>5<span class="cite-bracket">]</span></a></sup> (Emil Post 1920)<sup id="cite_ref-metalogic_2-2" class="reference"><a href="#cite_note-metalogic-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup></li>

<li>Proof of the syntactic completeness of truth-functional propositional logic (Emil Post 1920)<sup id="cite_ref-metalogic_2-3" class="reference"><a href="#cite_note-metalogic-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup></li>

<li>Proof of the decidability of truth-functional propositional logic (Emil Post 1920)<sup id="cite_ref-metalogic_2-4" class="reference"><a href="#cite_note-metalogic-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup></li>

<li>Proof of the consistency of first-order <a href="Monadic_predicate_calculus" title="Monadic predicate calculus">monadic predicate logic</a> (<a href="Leopold_L%C3%B6wenheim" title="Leopold Löwenheim">Leopold Löwenheim</a> 1915)</li>

<li>Proof of the semantic completeness of first-order monadic predicate logic (Leopold Löwenheim 1915)</li>

<li>Proof of the decidability of first-order monadic predicate logic (Leopold Löwenheim 1915)</li>

<li>Proof of the consistency of first-order predicate logic (<a href="David_Hilbert" title="David Hilbert">David Hilbert</a> and <a href="Wilhelm_Ackermann" title="Wilhelm Ackermann">Wilhelm Ackermann</a> 1928)</li>

<li>Proof of the semantic completeness of first-order <a href="Predicate_logic" class="mw-redirect" title="Predicate logic">predicate logic</a> (<a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness theorem</a> 1930)</li>

<li>Proof of the <a href="Cut-elimination_theorem" title="Cut-elimination theorem">cut-elimination theorem</a> for the <a href="Sequent_calculus" title="Sequent calculus">sequent calculus</a> (<a href="Gerhard_Gentzen" title="Gerhard Gentzen">Gentzen</a>'s <i>Hauptsatz</i> 1934)</li>

<li>Proof of the undecidability of first-order predicate logic (<a href="Entscheidungsproblem" title="Entscheidungsproblem">Church's theorem</a> 1936)</li>

<li><a href="G%C3%B6del's_incompleteness_theorems#First_incompleteness_theorem" title="Gödel's incompleteness theorems">Gödel's first incompleteness theorem</a> 1931</li>

<li><a href="G%C3%B6del's_incompleteness_theorems#Second_incompleteness_theorem" title="Gödel's incompleteness theorems">Gödel's second incompleteness theorem</a> 1931</li>

<li><a href="Tarski's_undefinability_theorem" title="Tarski's undefinability theorem">Tarski's undefinability theorem</a> (Gödel and Tarski in the 1930s)</li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .portalbox{padding:0;margin:0.5em 0;display:table;box-sizing:border-box;max-width:175px;list-style:none}.mw-parser-output .portalborder{border:1px solid var(--border-color-base,#a2a9b1);padding:0.1em;background:var(--background-color-neutral-subtle,#f8f9fa)}.mw-parser-output .portalbox-entry{display:table-row;font-size:85%;line-height:110%;height:1.9em;font-style:italic;font-weight:bold}.mw-parser-output .portalbox-image{display:table-cell;padding:0.2em;vertical-align:middle;text-align:center}.mw-parser-output .portalbox-link{display:table-cell;padding:0.2em 0.2em 0.2em 0.3em;vertical-align:middle}@media(min-width:720px){.mw-parser-output .portalleft{margin:0.5em 1em 0.5em 0}.mw-parser-output .portalright{clear:right;float:right;margin:0.5em 0 0.5em 1em}}

/* end https://en.wikipedia.org/ */

</style>

<ul><li><a href="Metalogic_programming" class="mw-redirect" title="Metalogic programming">Metalogic programming</a></li>

<li><a href="Metamathematics" title="Metamathematics">Metamathematics</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

<li id="cite_note-1"><span class="mw-cite-backlink"><b><a href="#cite_ref-1">^</a></b></span> <span class="reference-text">Harry Gensler, <a rel="nofollow" class="external text" href="https://books.google.com/books?id=jpteBwAAQBAJ">Introduction to Logic</a>, Routledge, 2001, p. 336.</span>

</li>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFHunter1996" class="citation book cs1"><a href="Geoffrey_Hunter_(logician)" title="Geoffrey Hunter (logician)">Hunter, Geoffrey</a> (1996) [1971]. <i>Metalogic: An Introduction to the Metatheory of Standard First-Order Logic</i>. University of California Press (published 1973). <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9780520023567</bdi>. <a href="OCLC_(identifier)" class="mw-redirect" title="OCLC (identifier)">OCLC</a> <a rel="nofollow" class="external text" href="https://search.worldcat.org/oclc/36312727">36312727</a>.</cite> (<a rel="nofollow" class="external text" href="https://archive.org/details/metalogicintrodu0000hunt">accessible to patrons with print disabilities</a>)</span>

</li>

<li id="cite_note-itslaia-3"><span class="mw-cite-backlink">^ <a href="#cite_ref-itslaia_3-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-itslaia_3-1"><sup><i><b>b</b></i></sup></a></span> <span class="reference-text"><a href="Rudolf_Carnap" title="Rudolf Carnap">Rudolf Carnap</a> (1958) <i><a rel="nofollow" class="external text" href="https://books.google.com/books?id=hAvVAgAAQBAJ">Introduction to Symbolic Logic and its Applications</a></i>, p. 102.</span>

</li>

<li id="cite_note-4"><span class="mw-cite-backlink"><b><a href="#cite_ref-4">^</a></b></span> <span class="reference-text"><cite id="CITEREFSmith2022" class="citation cs2">Smith, Robin (2022), <a rel="nofollow" class="external text" href="https://plato.stanford.edu/archives/win2022/entries/aristotle-logic/">"Aristotle's Logic"</a>, in Zalta, Edward N.; Nodelman, Uri (eds.), <i>The Stanford Encyclopedia of Philosophy</i> (Winter 2022 ed.), Metaphysics Research Lab, Stanford University<span class="reference-accessdate">, retrieved <span class="nowrap">2023-08-28</span></span></cite></span>

</li>

<li id="cite_note-reflections-5"><span class="mw-cite-backlink"><b><a href="#cite_ref-reflections_5-0">^</a></b></span> <span class="reference-text">Hao Wang, <a rel="nofollow" class="external text" href="https://books.google.com/books?id=wLLePwhDOMYC">Reflections on Kurt Gödel</a></span>

</li>

</ol></div>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><span class="noviewer" typeof="mw:File"></span> Media related to <a href="https://commons.wikimedia.org/wiki/Category:Metalogic" class="extiw external" title="commons:Category:Metalogic">Metalogic</a> at Wikimedia Commons</li>

<li><cite id="CITEREFDragalin2001" class="citation cs2">Dragalin, A.G. (2001) [1994], <a rel="nofollow" class="external text" href="https://www.encyclopediaofmath.org/index.php?title=Meta-logic">"Meta-logic"</a>, <i><a href="Encyclopedia_of_Mathematics" title="Encyclopedia of Mathematics">Encyclopedia of Mathematics</a></i>, <a href="European_Mathematical_Society" title="European Mathematical Society">EMS Press</a></cite></li></ul>

/* start https://en.wikipedia.org/ */

.mw-parser-output .hlist dl,.mw-parser-output .hlist ol,.mw-parser-output .hlist ul{margin:0;padding:0}.mw-parser-output .hlist dd,.mw-parser-output .hlist dt,.mw-parser-output .hlist li{margin:0;display:inline}.mw-parser-output .hlist.inline,.mw-parser-output .hlist.inline dl,.mw-parser-output .hlist.inline ol,.mw-parser-output .hlist.inline ul,.mw-parser-output .hlist dl dl,.mw-parser-output .hlist dl ol,.mw-parser-output .hlist dl ul,.mw-parser-output .hlist ol dl,.mw-parser-output .hlist ol ol,.mw-parser-output .hlist ol ul,.mw-parser-output .hlist ul dl,.mw-parser-output .hlist ul ol,.mw-parser-output .hlist ul ul{display:inline}.mw-parser-output .hlist .mw-empty-li{display:none}.mw-parser-output .hlist dt::after{content:": "}.mw-parser-output .hlist dd::after,.mw-parser-output .hlist li::after{content:" · ";font-weight:bold}.mw-parser-output .hlist dd:last-child::after,.mw-parser-output .hlist dt:last-child::after,.mw-parser-output .hlist li:last-child::after{content:none}.mw-parser-output .hlist dd dd:first-child::before,.mw-parser-output .hlist dd dt:first-child::before,.mw-parser-output .hlist dd li:first-child::before,.mw-parser-output .hlist dt dd:first-child::before,.mw-parser-output .hlist dt dt:first-child::before,.mw-parser-output .hlist dt li:first-child::before,.mw-parser-output .hlist li dd:first-child::before,.mw-parser-output .hlist li dt:first-child::before,.mw-parser-output .hlist li li:first-child::before{content:" (";font-weight:normal}.mw-parser-output .hlist dd dd:last-child::after,.mw-parser-output .hlist dd dt:last-child::after,.mw-parser-output .hlist dd li:last-child::after,.mw-parser-output .hlist dt dd:last-child::after,.mw-parser-output .hlist dt dt:last-child::after,.mw-parser-output .hlist dt li:last-child::after,.mw-parser-output .hlist li dd:last-child::after,.mw-parser-output .hlist li dt:last-child::after,.mw-parser-output .hlist li li:last-child::after{content:")";font-weight:normal}.mw-parser-output .hlist ol{counter-reset:listitem}.mw-parser-output .hlist ol>li{counter-increment:listitem}.mw-parser-output .hlist ol>li::before{content:" "counter(listitem)"\a0 "}.mw-parser-output .hlist dd ol>li:first-child::before,.mw-parser-output .hlist dt ol>li:first-child::before,.mw-parser-output .hlist li ol>li:first-child::before{content:" ("counter(listitem)"\a0 "}

/* end https://en.wikipedia.org/ */

</style><style data-mw-deduplicate="TemplateStyles:r1236075235">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbox{box-sizing:border-box;border:1px solid #a2a9b1;width:100%;clear:both;font-size:88%;text-align:center;padding:1px;margin:1em auto 0}.mw-parser-output .navbox .navbox{margin-top:0}.mw-parser-output .navbox+.navbox,.mw-parser-output .navbox+.navbox-styles+.navbox{margin-top:-1px}.mw-parser-output .navbox-inner,.mw-parser-output .navbox-subgroup{width:100%}.mw-parser-output .navbox-group,.mw-parser-output .navbox-title,.mw-parser-output .navbox-abovebelow{padding:0.25em 1em;line-height:1.5em;text-align:center}.mw-parser-output .navbox-group{white-space:nowrap;text-align:right}.mw-parser-output .navbox,.mw-parser-output .navbox-subgroup{background-color:#fdfdfd}.mw-parser-output .navbox-list{line-height:1.5em;border-color:#fdfdfd}.mw-parser-output .navbox-list-with-group{text-align:left;border-left-width:2px;border-left-style:solid}.mw-parser-output tr+tr>.navbox-abovebelow,.mw-parser-output tr+tr>.navbox-group,.mw-parser-output tr+tr>.navbox-image,.mw-parser-output tr+tr>.navbox-list{border-top:2px solid #fdfdfd}.mw-parser-output .navbox-title{background-color:#ccf}.mw-parser-output .navbox-abovebelow,.mw-parser-output .navbox-group,.mw-parser-output .navbox-subgroup .navbox-title{background-color:#ddf}.mw-parser-output .navbox-subgroup .navbox-group,.mw-parser-output .navbox-subgroup .navbox-abovebelow{background-color:#e6e6ff}.mw-parser-output .navbox-even{background-color:#f7f7f7}.mw-parser-output .navbox-odd{background-color:transparent}.mw-parser-output .navbox .hlist td dl,.mw-parser-output .navbox .hlist td ol,.mw-parser-output .navbox .hlist td ul,.mw-parser-output .navbox td.hlist dl,.mw-parser-output .navbox td.hlist ol,.mw-parser-output .navbox td.hlist ul{padding:0.125em 0}.mw-parser-output .navbox .navbar{display:block;font-size:100%}.mw-parser-output .navbox-title .navbar{float:left;text-align:left;margin-right:0.5em}body.skin--responsive .mw-parser-output .navbox-image img{max-width:none!important}@media print{body.ns-0 .mw-parser-output .navbox{display:none!important}}

/* end https://en.wikipedia.org/ */

</style></div><div role="navigation" class="navbox" aria-labelledby="Metalogic_and_metamathematics37" style="padding:3px"><table class="nowraplinks mw-collapsible autocollapse navbox-inner" style="border-spacing:0;background:transparent;color:inherit"><tbody><tr><th scope="col" class="navbox-title" colspan="2"><style data-mw-deduplicate="TemplateStyles:r1239400231">

/* start https://en.wikipedia.org/ */

.mw-parser-output .navbar{display:inline;font-size:88%;font-weight:normal}.mw-parser-output .navbar-collapse{float:left;text-align:left}.mw-parser-output .navbar-boxtext{word-spacing:0}.mw-parser-output .navbar ul{display:inline-block;white-space:nowrap;line-height:inherit}.mw-parser-output .navbar-brackets::before{margin-right:-0.125em;content:"[ "}.mw-parser-output .navbar-brackets::after{margin-left:-0.125em;content:" ]"}.mw-parser-output .navbar li{word-spacing:-0.125em}.mw-parser-output .navbar a>span,.mw-parser-output .navbar a>abbr{text-decoration:inherit}.mw-parser-output .navbar-mini abbr{font-variant:small-caps;border-bottom:none;text-decoration:none;cursor:inherit}.mw-parser-output .navbar-ct-full{font-size:114%;margin:0 7em}.mw-parser-output .navbar-ct-mini{font-size:114%;margin:0 4em}html.skin-theme-clientpref-night .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .navbar li a abbr{color:var(--color-base)!important}}@media print{.mw-parser-output .navbar{display:none!important}}

/* end https://en.wikipedia.org/ */

</style><div id="Metalogic_and_metamathematics37" style="font-size:114%;margin:0 4em"> and <a href="Metamathematics" title="Metamathematics">metamathematics</a></div></th></tr><tr><td colspan="2" class="navbox-list navbox-odd hlist" style="width:100%;padding:0;padding-left:2.0em;padding-right:2.0em;"><div style="padding:0 0.25em">

<ul><li><a href="Cantor's_theorem" title="Cantor's theorem">Cantor's theorem</a></li>

<li><i><a href="Entscheidungsproblem" title="Entscheidungsproblem">Entscheidungsproblem</a></i></li>

<li><a href="Church%E2%80%93Turing_thesis" title="Church–Turing thesis">Church–Turing thesis</a></li>

<li><a href="Consistency" title="Consistency">Consistency</a></li>

<li><a href="Effective_method" title="Effective method">Effective method</a></li>

<li><a href="Foundations_of_mathematics" title="Foundations of mathematics">Foundations of mathematics</a>

<ul><li><a href="Foundations_of_geometry" title="Foundations of geometry">of geometry</a></li></ul></li>

<li><a href="G%C3%B6del's_completeness_theorem" title="Gödel's completeness theorem">Gödel's completeness theorem</a></li>

<li><a href="G%C3%B6del's_incompleteness_theorems" title="Gödel's incompleteness theorems">Gödel's incompleteness theorems</a></li>

<li><a href="Soundness" title="Soundness">Soundness</a></li>

<li><a href="Completeness_(logic)" title="Completeness (logic)">Completeness</a></li>

<li><a href="Decidability_(logic)" title="Decidability (logic)">Decidability</a></li>

<li><a href="Interpretation_(logic)" title="Interpretation (logic)">Interpretation</a></li>

<li><a href="L%C3%B6wenheim%E2%80%93Skolem_theorem" title="Löwenheim–Skolem theorem">Löwenheim–Skolem theorem</a></li>

<li><a href="Metatheorem" title="Metatheorem">Metatheorem</a></li>

<li><a href="Satisfiability" title="Satisfiability">Satisfiability</a></li>

<li><a href="Independence_(mathematical_logic)" title="Independence (mathematical logic)">Independence</a></li>

<li><a href="Type%E2%80%93token_distinction" title="Type–token distinction">Type–token distinction</a></li>

<li><a href="Use%E2%80%93mention_distinction" title="Use–mention distinction">Use–mention distinction</a></li></ul>

</div></td></tr></tbody></table></div></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-04-10" href="https://en.wikipedia.org/wiki/?title=Metalogic&oldid=1284965171">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>